Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	0 + 0	→ 0
2:	0 + 1	→ 1
3:	0 + 2	→ 2
4:	0 + 3	→ 3
5:	0 + 4	→ 4
6:	0 + 5	→ 5
7:	0 + 6	→ 6
8:	0 + 7	→ 7
9:	0 + 8	→ 8
10:	0 + 9	→ 9
11:	1 + 0	→ 1
12:	1 + 1	→ 2
13:	1 + 2	→ 3
14:	1 + 3	→ 4
15:	1 + 4	→ 5
16:	1 + 5	→ 6
17:	1 + 6	→ 7
18:	1 + 7	→ 8
19:	1 + 8	→ 9
20:	1 + 9	→ c(1,0)
21:	2 + 0	→ 2
22:	2 + 1	→ 3
23:	2 + 2	→ 4
24:	2 + 3	→ 5
25:	2 + 4	→ 6
26:	2 + 5	→ 7
27:	2 + 6	→ 8
28:	2 + 7	→ 9
29:	2 + 8	→ c(1,0)
30:	2 + 9	→ c(1,1)
31:	3 + 0	→ 3
32:	3 + 1	→ 4
33:	3 + 2	→ 5
34:	3 + 3	→ 6
35:	3 + 4	→ 7
36:	3 + 5	→ 8
37:	3 + 6	→ 9
38:	3 + 7	→ c(1,0)
39:	3 + 8	→ c(1,1)
40:	3 + 9	→ c(1,2)
41:	4 + 0	→ 4
42:	4 + 1	→ 5
43:	4 + 2	→ 6
44:	4 + 3	→ 7
45:	4 + 4	→ 8
46:	4 + 5	→ 9
47:	4 + 6	→ c(1,0)
48:	4 + 7	→ c(1,1)
49:	4 + 8	→ c(1,2)
50:	4 + 9	→ c(1,3)
51:	5 + 0	→ 5
52:	5 + 1	→ 6
53:	5 + 2	→ 7
54:	5 + 3	→ 8
55:	5 + 4	→ 9
56:	5 + 5	→ c(1,0)
57:	5 + 6	→ c(1,1)
58:	5 + 7	→ c(1,2)
59:	5 + 8	→ c(1,3)
60:	5 + 9	→ c(1,4)
61:	6 + 0	→ 6
62:	6 + 1	→ 7
63:	6 + 2	→ 8
64:	6 + 3	→ 9
65:	6 + 4	→ c(1,0)
66:	6 + 5	→ c(1,1)
67:	6 + 6	→ c(1,2)
68:	6 + 7	→ c(1,3)
69:	6 + 8	→ c(1,4)
70:	6 + 9	→ c(1,5)
71:	7 + 0	→ 7
72:	7 + 1	→ 8
73:	7 + 2	→ 9
74:	7 + 3	→ c(1,0)
75:	7 + 4	→ c(1,1)
76:	7 + 5	→ c(1,2)
77:	7 + 6	→ c(1,3)
78:	7 + 7	→ c(1,4)
79:	7 + 8	→ c(1,5)
80:	7 + 9	→ c(1,6)
81:	8 + 0	→ 8
82:	8 + 1	→ 9
83:	8 + 2	→ c(1,0)
84:	8 + 3	→ c(1,1)
85:	8 + 4	→ c(1,2)
86:	8 + 5	→ c(1,3)
87:	8 + 6	→ c(1,4)
88:	8 + 7	→ c(1,5)
89:	8 + 8	→ c(1,6)
90:	8 + 9	→ c(1,7)
91:	9 + 0	→ 9
92:	9 + 1	→ c(1,0)
93:	9 + 2	→ c(1,1)
94:	9 + 3	→ c(1,2)
95:	9 + 4	→ c(1,3)
96:	9 + 5	→ c(1,4)
97:	9 + 6	→ c(1,5)
98:	9 + 7	→ c(1,6)
99:	9 + 8	→ c(1,7)
100:	9 + 9	→ c(1,8)
101:	x + c(y,z)	→ c(y,x + z)
102:	c(x,y) + z	→ c(x,y + z)
103:	c(0,x)	→ x
104:	c(x,c(y,z))	→ c(x + y,z)

There are 51 dependency pairs:


105:	1 +# 9	→ C(1,0)
106:	2 +# 8	→ C(1,0)
107:	2 +# 9	→ C(1,1)
108:	3 +# 7	→ C(1,0)
109:	3 +# 8	→ C(1,1)
110:	3 +# 9	→ C(1,2)
111:	4 +# 6	→ C(1,0)
112:	4 +# 7	→ C(1,1)
113:	4 +# 8	→ C(1,2)
114:	4 +# 9	→ C(1,3)
115:	5 +# 5	→ C(1,0)
116:	5 +# 6	→ C(1,1)
117:	5 +# 7	→ C(1,2)
118:	5 +# 8	→ C(1,3)
119:	5 +# 9	→ C(1,4)
120:	6 +# 4	→ C(1,0)
121:	6 +# 5	→ C(1,1)
122:	6 +# 6	→ C(1,2)
123:	6 +# 7	→ C(1,3)
124:	6 +# 8	→ C(1,4)
125:	6 +# 9	→ C(1,5)
126:	7 +# 3	→ C(1,0)
127:	7 +# 4	→ C(1,1)
128:	7 +# 5	→ C(1,2)
129:	7 +# 6	→ C(1,3)
130:	7 +# 7	→ C(1,4)
131:	7 +# 8	→ C(1,5)
132:	7 +# 9	→ C(1,6)
133:	8 +# 2	→ C(1,0)
134:	8 +# 3	→ C(1,1)
135:	8 +# 4	→ C(1,2)
136:	8 +# 5	→ C(1,3)
137:	8 +# 6	→ C(1,4)
138:	8 +# 7	→ C(1,5)
139:	8 +# 8	→ C(1,6)
140:	8 +# 9	→ C(1,7)
141:	9 +# 1	→ C(1,0)
142:	9 +# 2	→ C(1,1)
143:	9 +# 3	→ C(1,2)
144:	9 +# 4	→ C(1,3)
145:	9 +# 5	→ C(1,4)
146:	9 +# 6	→ C(1,5)
147:	9 +# 7	→ C(1,6)
148:	9 +# 8	→ C(1,7)
149:	9 +# 9	→ C(1,8)
150:	x +# c(y,z)	→ C(y,x + z)
151:	x +# c(y,z)	→ x +# z
152:	c(x,y) +# z	→ C(x,y + z)
153:	c(x,y) +# z	→ y +# z
154:	C(x,c(y,z))	→ C(x + y,z)
155:	C(x,c(y,z))	→ x +# y

The approximated dependency graph contains one SCC: {150-155}.

Consider the SCC {150-155}. The constraints could not be solved.

Tyrolean Termination Tool (37.19 seconds) --- May 4, 2006